| Definitions |  b, fpf-dom(eq; x; f), top, ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-trans(x), ecl-trans-tuple{i:l}(ds; da), x:A  B(x), ecl-trans-type(A), ecl-trans-ks(v), ecl-trans-a(v), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), R-state-var-init(i; ds; da; x; T; v; ks; tr), ecl-machine2(i; ds; da; x; T; ks; a; upd),  ,  , inl x ,  x.A(x), list_accum(x,a.f(x;a); y; l), let x,y = A in B(x;y), if b then t else f fi , f(a), fpf-cap(f; eq; x; z), product-deq(A; B; a; b), Kind-deq, <a, b>, [], Knd, decl-state(ds), ma-valtype(da; k), Rall(L; x.R(x)), fpf-ap(f; eq; x), {x:A| B(x)} , (x  l), fpf-join(eq; f; g), id-deq, mkid{$x:ut2}, fpf-single(x; v),  x. t(x), update-spec-vars(upd), Rplus(left; right), Rinit(loc; T; x; v), R-state-var(i; ds; da; x; T; ks; tr), P   Q, strong-subtype(A; B),  x:A. B(x), R-compat{i:l}(A; B), x:A  B(x), type List,  A, update-spec-decl(upd; ds), update-spec(ds; da), ecl(ds; da), fpf(A; a.B(a)), Id, Type, prop{i:l}, s = t, t T,  , R-has-loc(R; i), subtype(S; T), grp_car(g), l[i], ||as||, A  B, #$n, p-outcome(p), P  Q, decision, eqof(d), es-dt(l; da), x,y. t(x;y), rationals, decl-type{i:l}(ds; x), A c B, es realizer ind Reffect compseq tag def, Rnone, R-lnk-tags(ds; da; l; tgs; ks; g), Rlist(L), inr x , R-loc(R), Rds(R), Rda(R), R-base-domain(R), eq_bd(p; q), R-frame-compat(A; B), R-interface-compat(A; B), Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Reffect-ds(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), Rsends-g(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rrframe?(x1), Rrframe-x(x1), Rpre-ds(x1), Rpre-a(x1), Rrframe-L(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), Rsends-knd(x1), Rsends-l(x1), Rsends-dt(x1), Rsends-T(x1), es realizer ind, left + right, Unit,  , tt, ff, sqequal(s; t), sq_type(T), P  Q, P Q, P Q, IdLnk, EqDecider(T), isect(A; x.B(x)), fpf-empty, bor(p; q), band(p; q), bimplies(p; q),  b, deq-member(eq; x; L), eq_id(a; b), eq_lnk(a; b), qeq(r; s), q_less(a; b), q_le(r; s), eq_atom{$n:n}(x; y), dcdr-to-bool(d), grp_blt(g; a; b), x f y, set_blt(p; a; b), null(as), eq_atom(x; y), (i = j), i z j, i <z j, eq_bool(p; q), R-discrete_compat(A; B), Reffect-discrete(A), Rinit-discrete(A), Reffect?(x1), Reffect-x(x1), Reffect-f(x1), Rinit?(x1), Rinit-x(x1), Rinit-v(x1), es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, True, R-Feasible{i:l}(R), fpf-compatible(A; a.B(a); eq; f; g),  , a < b, void, rec(x.A(x)), locl(a), guard(T), rcv(l,tg), Reffect(loc; ds; knd; T; x; f), Rframe(loc; T; x; L), es_realizer{i:l}, case b of inl(x) => s(x) | inr(y) => t(y),  x:A. B(x), False, atom{$n:n}, t.1, t.2, x(s),  T, fpf-sub(A; a.B(a); eq; f; g) |
| Lemmas | fpf-single-dom, or functionality wrt iff, subtype rel self, fpf-cap-join-subtype, subtype rel dep function, ext-eq weakening, subtype rel weakening, nat properties, fpf-sub weakening, fpf-sub-join-left2, subtype-fpf-cap-top, deq wf, squash wf, list accum wf, product-deq wf, pi2 wf, pi1 wf, R-discrete compat wf, Rframe wf, fpf-empty wf, Kind-deq wf, fpf-empty-compatible-right, assert-eq-id, rev implies wf, iff wf, Id sq, guard wf, fpf-compatible-singles, fpf-compatible-symmetry, true wf, fpf-compatible wf, bool wf, eq id wf, bnot wf, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, R-compat-symmetry, R-compat-disjoint, btrue wf, Reffect wf, ma-valtype wf, fpf-single wf, fpf-compatible-single, fpf-single wf3, fpf-compatible-join2, fpf-cap wf, decl-type wf, ifthenelse wf, eqof eq btrue, fpf-cap-single, fpf-join-cap-sq, decl-state wf, rationals wf, R-compat-Rall2, IdLnk wf, R-compat-Rplus-sq, false wf, fpf-join-dom2, R-state-var-compat-unequal-loc, fpf-compatible-single-iff, fpf-compatible-self, fpf-compatible-join, fpf-compatible-single2, select wf, length wf1, nat wf, R-state-var-compat3, R-compat-Rall, R-compat wf, Rplus wf, R-state-var wf, Rinit wf, Rall wf, Id wf, update-spec-vars wf, fpf-join wf, id-deq wf, fpf-ap wf, l member wf, ecl-trans-tuple wf, ecl-trans wf, fpf wf, Knd wf, ecl wf, update-spec wf, update-spec-decl wf, ecl-trans-type wf, member wf, fpf-trivial-subtype-top, subtype rel wf, top wf, fpf-dom wf, assert wf, not wf, ecl-machine1 wf, ecl-machine2 wf |
